COMMENT ⊗   VALID 00005 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.s(PROVEX,|PROOFS: EXAMPLES|)
C00003 00003	.ss(samefr,The SAMEFRINGE problem.)
C00020 00004	.ss(partn, Correctness of a program to partition lists.)
C00045 00005	.ss(provexex, Exercises )
C00052 ENDMK
C⊗;
.s(PROVEX,|PROOFS: EXAMPLES|)
.if NOTASSEMBLING then start
.IMPURE: NEXT SECTION!;
.MACHIN: NEXT SECTION!;
.SEARCH: NEXT SECTION!;
.EXTEND: NEXT SECTION!;
.ABSNTX: NEXT SECTION!;
.COMPIL: NEXT SECTION!;
.COMPUT: NEXT SECTION!;
.end

	In this section we present some non-trivial examples illustrating
the methods developed in Chapter {section PROVIN}.

.ss(samefr,The SAMEFRINGE problem.)
 
	As a substantial application of the techniques described in 
Chapter {section PROVIN}, we will give a proof of correctness of the predicate 
⊗samefringe which has been presented as a solution of the SAMEFRINGE problem.  
This is the problem of determining whether or not two S-expressions have the 
same fringe using a minimum of space.  We will be concerned only with the 
correctness of ⊗samefringe since the efficiency is not an ⊗extensional property.  

	We have already studied two programs for computing the fringe of an
S-expression, namely ⊗fringe and ⊗flatten, which were proved to compute
the same function from S-expressions to non-empty lists.
The predicate ⊗samefringe is computed by the LISP program
.begin nofill turnon "∂" group
.n←15

$SAMEFR: ∂(n)⊗⊗samefringe[x, y] ← ⊗
	 ∂(n+4)⊗⊗x qequal y qor [qnot qat x qand qnot qat y qand same[gopher x, gopher y]]⊗
where
$SAME:   ∂(n)⊗⊗same[x, y] ← qa x qequal qa y qand samefringe[qd x, qd y]⊗
and
$GOPHER: ∂(n)⊗⊗gopher x ← qif qat qa x qthen x qelse gopher [qaa x . [qda x . qd x]]⊗.
.end

What we want to show is that ⊗samefringe says "yes" for input ⊗⊗x,y⊗ just when
⊗⊗fringe_x=fringe_y⊗.   To do this we use the ideas of 
Chapter {subsection recpred!}.  We first represent 
the above programs by functions ⊗samefringef, ⊗samef, and ⊗gopher satisfying
the axioms:
.begin nofill turnon "∂" group
.n←15

$SAMEFR-DEF: ∂(n)⊗⊗∀x y: samefringef[x, y] = ⊗
	     ∂(n+8)⊗⊗x qequal y qor [qnot qat x qand qnot qat y qand same[gopher x, gopher y]]⊗
$SAME-DEF:   ∂(n)⊗⊗∀x y: same[x, y] = qa x qequal qa y qand samefringef[qd x, qd y]⊗
$GOPHER-DEF: ∂(n)⊗⊗∀x: gopher x ← qif qat qa x qthen x qelse gopher [qaa x . [qda x . qd x]]⊗.
.end

We then define the predicate ⊗samefringe by

$SAMEFRINGE-DEF ___⊗⊗∀x y: [samefringe[x,y] ≡ True samefringef[x,y]]⊗

and the statement of correctness becomes

$SAMEFRINGE-COR: __⊗⊗∀x y: [samefringe[x,y] ≡ fringe x=fringe y].⊗

The program computing ⊗samefringe divides pairs ⊗⊗x,y⊗ of S-expressions into
two cases: $ATOMXY where ⊗⊗ATOM_x_∨_ATOM_y⊗ and $PAIRXY where 
⊗⊗PAIR_x_∧_PAIR_y⊗.  And we have two immediate corollaries of
$SAMEFR-DEF and $SAME-DEF.  
.begin nofill turnon "∂" group
.n←15

$SFF-ATOMXY: ∂(n)⊗⊗∀x y: [ATOM x ∨ ATOM y] ⊃ samefringef[x,y] = x qequal y⊗
$SFF-PAIRXY: ∂(n)⊗⊗∀xx yy: samefringef[xx,yy] = ⊗
                  ∂(n+6) ⊗⊗qa gopher xx qequal qa gopher yy qand samefringef[qd gopher xx, qd gopher y]⊗
.end

Since recursive calls occur only in the $PAIRXY case and are of the form 
⊗⊗samefringef[qd gopher_xx,qd gopher_yy]⊗ this suggests that to prove
properties of ⊗samefringef (and of ⊗⊗samefringe⊗) we need to find a rank
function ⊗⊗qrho[x,y]⊗ such that 

⊗⊗⊗∀xx yy: qrho[qd gopher xx,qd gopher yy] < qrho[xx,yy].⊗ 

Proof can then be done using induction on the rank as explained in
Chapter {subsection induction!}.

Recall that we proved in Chapter {subsection induction!}
.begin nofill turnon "∂" group
.n←15

$PAIR-GOPHER: ∂(n)⊗⊗∀xx: PAIR_gopher xx⊗
$SIZE-GOHPER: ∂(n)⊗⊗∀xx: size gopher xx = size xx⊗
.end

Thus either ⊗⊗qrho[x,y]=size x+size y⊗ or simply ⊗⊗rho[x,y] = size x⊗ will
do as a rank function for ⊗samefringe.  
Since for either version of qrho we have 

⊗⊗⊗∀xx yy: qrho[qd gopher xx,qd gopher yy] < qrho[xx,yy]⊗

we see that to prove ⊗⊗x y: qP[x,y]⊗ by on rank it is sufficient to prove
.begin nofill turnon "∂" group
.n←15

$PHI-ATOMXY: ∂(n)⊗⊗∀ x y: [ATOM x ∨ ATOM y]⊃qP[x,y]⊗ 
and
$PHI-PAIRXY: ∂(n)⊗⊗∀xx yy: qP[qd gopher xx,qd gopher yy] ⊃ qP[xx,yy]⊗
.end

	To prove that correctness of ⊗samefringe we first prove that
the program terminates on all S-expression pairs, thus giving up
a complete description of the predicate.  Thus we prove by induction on
the rank qrho that
.begin nofill turnon "∂" group
.n←15

$S-SAMEFR: ∂(n)⊗⊗∀x y: SEXP samefringef[x,y].⊗

which according to the above discussion reduces to proving 

$S-ATOMXY: ∂(n)⊗⊗∀ x y: [ATOM x ∨ ATOM y]⊃SEXP samefringef[x,y]⊗
and
$S-PAIRXY: ∂(n)⊗⊗∀xx yy: SEXP samefringef[qd gopher xx,qd gopher yy] ⊃ 
SEXP samefringef[xx,yy]⊗
.end

$S-ATOMXY follows directly from $SFF-ATOMXY and the domain map for qequal 
and $S-PAIRXY follows directly from $SFF-PAIRXY,PAIR-GOPHER, 
and the domain maps for qequal and qand.

We now obtain a characterization of ⊗samefringe in the two cases 
⊗ATOMXY and ⊗PAIRXY.   
.begin nofill turnon "∂" group
.n←14

$SF-ATOMXY: ∂(n)⊗⊗∀x y: [[ATOM x ∨ ATOM y] ⊃ samefringe[x,y] ≡ x = y]⊗
$SF-PAIRXY: ∂(n)⊗⊗∀xx yy: [samefringe[xx,yy] ≡ ⊗
                  ∂(n+8) ⊗⊗qa gopher xx = qa gopher yy ∧ samefringe[qd gopher xx, qd gopher y] ]⊗
.end

These facts follow directly from 
$SAMEFRINGE-DEF,SFF-ATOMXY,SFF-PAIRXY,S-SAMEFR,PAIR-GOPHER, 
and the $EQ- theorems given in Chapter {subsection recpred!}.

Now we are ready to prove $SAMEFRINGE-COR.  Using the same induction principle
as for $S-SAMEFR we see that we need only prove 
.begin nofill turnon "∂" group
.n←15

$COR-ATOMXY: ∂(n)⊗⊗∀ x y: [[ATOM x ∨ ATOM y]⊃[samefringe[x,y]≡fringe x=fringe y]]⊗
and
$COR-PAIRXY: ∂(n)⊗⊗∀xx yy: [[samefringe[qd gopher xx,qd gopher yy]≡ ⊗
		     ∂(n+8)⊗⊗fringe qd gopher xx=fringe qd gopher yy] ⊃ ⊗
             ∂(n+6)⊗⊗[samefringe[xx,yy]≡fringe xx=fringe yy] ]⊗
.end

In order to complete the proof we need some lemmas about ⊗fringe and ⊗gopher: 
.begin nofill turnon "∂" group
.n←20

$FRINGE-ATOMXY: ∂(n)⊗⊗∀ x y: [[ATOM x ∨ ATOM y]⊃[fringe x=fringe y≡x=y]]⊗
$CAR-GOPHER-FRINGE: ∂(n)⊗⊗∀xx: qa fringe xx = qa gopher xx⊗
$CDR-GOHPER-FRINGE: ∂(n)⊗⊗∀xx: qd fringe xx = fringe qd gopher xx⊗
.end

$CAR-GOPHER-FRINGE and $CDR-GOHPER-FRINGE were given as exercises in 
Chapter {subsection induction!}.
$FRINGE-ATOMXY follows easily from ⊗⊗∀x_a:_[fringe_x=fringe_a≡x=a]⊗
Which can be proved as follows.  If ⊗x is an atom
Then by $FRINGE-ATOM we need only show ⊗⊗<x>=<a>≡x=a⊗ which is follows
from $EQPAIR (proved in Chapter {subsection sexpth!}).
If ⊗x is not an atom then ⊗⊗ATOM∩PAIR=qEMPTY⊗ tells us that ⊗⊗x≠a⊗ and
we need only show ⊗⊗fringe x≠<a>⊗.  One way to see this is to observe
that ⊗⊗qd <a>=qNIL⊗ and ⊗⊗NELIST qd fringe x⊗.  We leave the details
to the reader.

	Now to complete the proof of $COR-SAMEFRINGE.  $COR-ATOMXY follows
directly from $SF-ATOMXY and $FRINGE-ATOMXY.  
To prove $COR-PAIRXY we assume

⊗⊗⊗samefringe[qd gopher xx,qd gopher yy]≡fringe qd gopher xx=fringe qd gopher yy] ⊗

then by $SF-PAIRXY it is sufficient to prove

⊗⊗⊗[qa gopher xx=qa gopher yy ∧ fringe qd gopher xx=fringe qd gopher yy]≡fringe xx=fringe yy⊗

Using $CAR-GOPHER-FRINGE and $CDR-GOPHER-FRINGE this reduces to:

⊗⊗⊗[qa fringe xx=qa fringe yy ∧ qd fringe xx=qd fringe yy]≡fringe xx=fringe yy⊗

which is just $EQPAIR.  

	Another version of ⊗samefringe without any auxiliary functions is

.begin nofill turnon "∂" group
.n←10

$SAMEFR1: ∂(n)⊗⊗samefringe[x, y] ← ⊗
          ∂(n+4)⊗⊗x qequal y qor ⊗
          ∂(n+4)⊗⊗[qnot qat x qand qnot qat y qand ⊗
            ∂(n+6)⊗⊗[qif qat qa x qthen [qif qat qa y qthen qa x qequal qa y qand samefringe[qd x,qd y] ⊗
                                ∂(n+16)⊗⊗qelse samefringe[x,qaa y. [qda y . qd y]]]⊗
            ∂(n+6)⊗⊗ qelse samefringe[qaa x . [qda x . qd x], y]. ⊗
.end

Note that a recursive call to ⊗samefringe does one of the following three things:
.begin nofill

	1)  decreases  ⊗⊗size x + size y⊗
	2)  leaves  ⊗⊗size x + size y⊗ and ⊗⊗size qa x⊗ invariant and decreases ⊗⊗size qa y⊗
	3)  leaves  ⊗⊗sixe x + size y⊗ and ⊗⊗size qa y⊗ invariant and decreases ⊗⊗size qa x ⊗.
.end
.TURN ON "↑[]"
This can lead to a choice of an induction axiom schema in at least two ways.
If in the $NUMINDUCTION-CVI schema we let ⊗n and ⊗m range over all ordinals less
than a given one it becomes a schema of transfinite induction. Ordinary induction
is obtained as a special case where the bounding ordinal is qW the least transfinite
ordinal.  If we take the bounding ordinal to be qW↑[qW] then the SAMEFRINGE theorem
for the above version of ⊗samefringe can be proved using the predicate
.TURN OFF

⊗⊗⊗qP n  ≡ ∀x y: [[size x +size y]qW + size qa x + size qa y = n ⊃ $$THM$[x, y]]⊗


	Alternately one could axiomatize the lexicographic ordering of triples
of numbers by
.NOFILL

⊗⊗⊗∀l%41%* m%41%* n%41%* l m n: [(l%41%*, m%41%*, n%41%*) < (l, m, n) ≡				⊗
⊗⊗⊗[l%41%* < l] ∨ [l%41%* = l ∧ m%41%* < m] ∨ [l%41%* = l ∧ m%41%* = m ∧ n%41%* < n]]⊗
.FILL
This ordering is well-founded (has no infinite decreasing sequences) and so we
have a schema analogous to $NUMINDUCTION-CVI given by
.NOFILL

⊗⊗⊗∀l m n: [∀l%41%* m%41%* n%41%*: [(l%41%*, m%41%*, n%41%*) < (l, m, n) ⊃qP(l%41%*, m%41%*, n%41%*)] ⊃ qP(l, m, n)]⊗
⊗⊗⊗⊃ ∀l m n: qP(l, m, n)⊗
.FILL
The SAMEFRINGE theorems can now be proved using this schema with the predicate

⊗⊗⊗qP(l, m, n) ≡ ∀x y: [l = size x +size y ∧ m = size qa y ∧ n = size qa x ⊃ $$THM$[x, y]]⊗


	The minimization schema provides an alternate method for proving the 
correctness of ⊗samefringe.  To simplify matters we eliminate the auxiliary
function ⊗same from the definition of ⊗samefringe thus eliminating the problem
of having to deal with mutually recursive programs.  The functional defining
⊗samefringe now becomes
.begin nofill turnon "∂" group
.n←10

∂(n)⊗⊗qt%4sf%* = λf: λx y: [[x qequal y] qor [[qnot qat x qand qnot qat y] qand⊗
         ∂(n+8)⊗⊗[[qa gopher x qequal qa gopher y] qand f[qd gopher x,qd gopher y]]]] ⊗.
.end

Now we form an axiom schema from the minimization schema by using the qt%4sf%*
given above and ⊗samefringe for ⊗f. 

⊗⊗⊗∀x y: [SEXP qt%4sf%*[F,x,y] ⊃ F[x,y] = qt%4sf%*[F,x,y]] ⊃ 
∀x y: [SEXP samefringe[x,y] ⊃ samefringe[x,y] = F[x,y]] ⊗.

We instantiate this schema with 

⊗⊗⊗F[x, y] = fringe x qequal fringe y  .		⊗

.XGENLINES←XGENLINES-2

The proof then consists of the following steps
.begin nofill group

Prove
	1)	⊗⊗∀x y: [F[x, y] = qt%4sf%*[F] [x, y]]⊗
	2)	⊗⊗∀x y:[SEXP samefringef[x,y]⊗
conclude from 1) - 2) and the minimization schema instantiatio
	3)	⊗⊗∀x y: [fringe x qequal fringe y = samefringef[x, y]]⊗
and from the definition of ⊗samefringe 2) and 3) conclude
	5)	⊗⊗∀x y: [samefringe[x, y] ≡ fringe x = fringe y]⊗
as desired.
.end

.ss(partn, Correctness of a program to partition lists.)

	Consider the problem of determining all partitions
of a list into some number of (non-empty) sublists.
We say that a list ⊗w is a partition of another list ⊗u into ⊗n parts 
if:

.begin nofill group
.item←0
.indent 5,5

#. each element of ⊗w is a nonempty list,
#. the length of ⊗w is ⊗n, and
#. the result of ⊗⊗append⊗ing the elements of ⊗w together (in order) is ⊗u. 
.end

Thus $$((A B) (C) (D))$ 
is a partition of the list $$(A B C D)$ into 3 parts, and 

⊗⊗⊗$$(((A B) (C) (D)) ((A) (B C) (D)) ((A) (B) (C D)))$⊗

is the list of all partitions of $$(A B C D)$ into 3 parts.
Note that for lists the order of the elements of the partition is
important, in contrast the usual notion of partitions of a natural 
number into a list of summands.

       In order to make the discussion of partitions easier, we will introduce some
new sorts: ⊗UULIST (lists whose members are non-empty lists) made up of the
subsorts ⊗NEUULIST (non-empty lists of non-empty lists) and ⊗NULL,  
⊗PNLIST (partition lists, e.g. the members are of sort ⊗⊗UULIST⊗)
made up of the subsorts ⊗NEPNLIST and ⊗NULL, 
and ⊗PNNLIST (non trivial partition lists, e.g. the members are of sort ⊗⊗NEUULIST⊗)
made up of the subsorts ⊗NEPNNLIST and ⊗NULL.  
We will have additional variables ranging over the new sorts.
.begin nofill turnon "∂"
.n←20
.group

∂(n)⊗⊗uul, vvl, wwl ε UULIST⊗
∂(n)⊗⊗uull, vvll, wwll ε NEUULIST⊗
∂(n)⊗⊗pl, ql, rl ε PNLIST⊗
∂(n)⊗⊗pll, qll, rll ε NEPNLIST⊗
∂(n)⊗⊗pnnl, qnnl, rnnl ε PNNLIST⊗
∂(n)⊗⊗pnnll, qnnll, rnnll ε NEPNNLIST⊗
.end

And we will have definition of programs by recursion on the new domains
(analogous to ordinary list recursion) and corresponding structural
induction principles.   A formal description of the new sorts
is given at the end of this section.



	In order to formalize the notion of a partition, we need to specify
what is meant by the phrase "appending elements of a list together".
The program ⊗combine appends together the elements of a partition and
is defined using ⊗UULIST recursion by:

⊗⊗⊗combine uul ← qif qn uul qthen qNIL qelse qa uul * combine qd uul⊗

and represented by the function ⊗combine which satisfies the axiom:
.begin nofill turnon "∂"
.n←10

$COMBINE: ⊗⊗⊗∀uul: combine uul = qif qn uul qthen qNIL qelse qa uul * combine qd uul⊗

from which we easily deduce

∂(n)$COMBINE-NIL: ⊗⊗combine qNIL = qNIL⊗
∂(n)$COMBINE-ULL: ⊗⊗∀uull: combine uull =qa uull * combine qd uull⊗
.end

If we restrict the domain of ⊗append to ⊗UULIST ⊗PNLIST or ⊗PNNLIST 
we obtain the additional domain mappings for ⊗append:  
.begin nofill turnon "∂"
.n←20

∂(n)⊗⊗*: UULIST qcross UULIST → UULIST⊗
∂(n)⊗⊗*: PNLIST qcross PNLIST → PNLIST⊗
∂(n)⊗⊗*: PNNLIST qcross PNNLIST → PNNLIST⊗

Using the facts specfied by the function mappings for ⊗append we have

∂(n)⊗⊗combine: UULIST → LIST⊗
∂(n)⊗⊗combine: NEUULIST → NELIST⊗
.end

Now we can give a formal definition of what we mean by partition.
We introduce the predicate ⊗Ispartn with the defining axiom

.begin nofill 

$ISPARTN-DEF: 
⊗⊗⊗∀U N W:[Ispartn[W,U,N] ≡ ∃uul.(W =uul ∧ length uul = N ∧ combine uul = U]]⊗
.end

which is a direct formalization of the three properties of a partition given above.
Given a list ⊗u and a number ⊗n we want a list ⊗pl of all partitions of
⊗u into ⊗n parts. 

	Before we give the program computing ⊗pl, 
we analyze some properties of partitions of a list.  
First, the degenerate cases where ⊗u is qNIL or ⊗n is $0.  
If ⊗⊗u = qNIL⊗ then it can not be partitioned into non-empty lists, so
the only possibility is the partition which itself is qNIL partitioning of
⊗u into $0 parts.  If ⊗u is non-empty then there must be 
at least $1 part in the partition, e.g. ⊗⊗n ≠ 0⊗.  This is expressed
by the following lemmas.
Also note that in the definition of ⊗Ispartn, 
if ⊗⊗n ≠ 0⊗ we may choose the ⊗UULIST to be non-empty.

.begin nofill turnon "∂"
.n←5

∂(n)$ISPARTN-NIL-ZERO: ⊗⊗∀W:[Ispartn[W,qNIL,0] ≡ W = qNIL]⊗
∂(n)$ISPARTN-NIL-NN: ⊗⊗∀nn W:¬Ispartn[W,qNIL,nn]⊗
∂(n)$ISPARTN-UU-ZERO: ⊗⊗∀uu W:¬Ispartn[W,uu,0]⊗
∂(n)$ISPARTN-DEF-NN: 
∂(n+8)⊗⊗∀uu nn W:[Ispartn[W,uu,nn]≡∃uull:[W=uull∧length uull=nn∧combine uull=uu]]⊗

.end

These lemmas are easily proved using the definitions of ⊗Ispartn, 
⊗length and ⊗combine, the fact that the only the empty list has
length 0 and only the empty list of non-empty lists combines
into qNIL.

	Now we consider non-trivial partitions of non-empty lists.  
Consider a partition ⊗uull of the non-empty list ⊗uu into ⊗nn parts. 
Let ⊗⊗ww=qa uull⊗.  Note that ⊗ww must be and initial segment of ⊗uu.  
There are two posibilities. Either ⊗ww is the one element list ⊗⊗<qa uu>⊗,
or it is a list of length greater than one (e.g. ⊗⊗qa ww=qa uu⊗ and
⊗⊗qd ww≠qNIL⊗.  In the first case ⊗⊗qd uull⊗ is a partition of 
⊗⊗qd uu⊗ into ⊗⊗sub1 nn⊗ parts.
In the second case the list formed by replacing ⊗ww by ⊗⊗qd ww⊗ 
(in ⊗⊗W⊗) is a partition of ⊗⊗qd uu⊗ into ⊗nn parts.   Thus we have
.begin nofill turnon "∂"
.n←4

∂(n)$ISPARTN-UU-NN: 
∂(n+8)⊗⊗∀uu nn W:[Ispartn[W,uu,nn] ≡ ⊗
∂(n+12)⊗⊗∃uull:[W=uull∧qa uull=<qa uu>∧Ispartn[qd uull,qd uu,sub1 nn]] ∨⊗
∂(n+12)⊗⊗∃uull:[W=uull∧qaa uull=qa uu∧Ispartn[[qda uull_._qd uull],qd uu,nn]]⊗
.end

The proof of $ISPARTN-UU-NN uses just the definitions of ⊗Ispartn, ⊗length, 
and ⊗combine together with basic facts about numbers and S-expressions.
By $ISPARTN-DEF-NN it is sufficient to show
.begin nofill 

__⊗⊗∃uull:[W=uull ∧ length uull=nn ∧ combine uull=uu]⊗ 
__⊗⊗ ≡ ∃uull:[W=uull∧qa uull=<qa uu>∧Ispartn[qd uull,qd uu,sub1 nn]] ∨⊗
__⊗⊗___∃uull:[W=uull∧qaa uull=qa uu∧Ispartn[[qda uull_._qd uull],qd uu,nn]]⊗
.end

First assume 

$ISUUNN1: ⊗⊗⊗W=uull ∧ length uull=nn and combine uull=uu⊗.  

Then if we subsitute ⊗⊗combine uull⊗ for ⊗uu and use $COMBINE-ULL, $APPEND-UU 
and the basic facts about S-expressions we obtain ⊗⊗qa uull=qa uu_._qda uull⊗ 
In the case: ⊗⊗qda uull=qNIL⊗ we will show
.begin nofill

⊗⊗ ∃vvll:[W=vvll∧qa vvll=<qa uu>∧Ispartn[qd vvll,qd uu,sub1 nn]] ⊗

and in the case: ⊗⊗qda uull≠qNIL⊗  we will show 

⊗⊗ ∃vvll:[W=vvll∧qaa vvll=qa uu∧Ispartn[[qda vvll_._qd vvll],qd uu,nn]]⊗
.end

thus proving the => direction of the equivalence.  Assume ⊗⊗qda uull=qNIL⊗
then if we let ⊗uul=qd uull⊗ we have by 
$APPEND-NIL, $APPEND-UU, $LENGTH-UU, $COMBINE-ULL and 
basic properties of numbers and S-expressions

⊗⊗⊗uul=qd uull ∧ length uul=sub1 nn ∧ combine uul=qd uu⊗

and by $ISPARTN-DEF  

⊗⊗⊗W=uull ∧ qd uull=[qa uu_._qNIL]∧Ispartn[qd uull,qd uu,sub1 nn]⊗

completing the first case.  Now assume ⊗⊗qda uull≠qNIL⊗.  Let ⊗⊗qda uull=ww⊗
and ⊗⊗[ww_.qd uull]=wwll⊗.  Then as above we have

⊗⊗⊗ cons(cdr car uull,cdr uull)=wwll ∧ length wwll=nn ∧ combine wwll=qd uu⊗

and by $ISPARTN-DEF  

⊗⊗⊗W=uull ∧ qaa uull=qa uu ∧ Ispartn[qda uull_._qd uull,qd uu,nn]⊗ 

completing the second case and the proof of the => direction.

To prove the <= direction there are also two cases:
.begin nofill

__⊗⊗∃uull:[W=uull∧qa uull=<qa uu>∧Ispartn[qd uull,qd uu,sub1 nn]] ⊃⊗
__⊗⊗∃uull:[W=uull ∧ length uull=nn ∧ combine uull=uu] ⊗
and
__⊗⊗∃uull:[W=uull∧qaa uull=qa uu∧Ispartn[[qda uull_._qd uull],qd uu,nn]] ⊃⊗
__⊗⊗∃uull:[W=uull ∧ length uull=nn ∧ combine uull=uu].⊗
.end

If we assume 
.begin nofill

⊗⊗⊗ W=uull∧qa uull=<qa uu>∧Ispartn[qd uull,qd uu,sub1 nn] ⊗
or
⊗⊗⊗ W=uull∧qaa uull=qa uu∧Ispartn[[qda uull_._qd uull],qd uu,nn]] ⊗

then by $ISPARTN-DEF, $APPEND-NIL, $APPEND-UU, $LENGTH-UU, $COMBINE-ULL we have

⊗⊗⊗W=uull ∧ length uull=nn ∧ combine uull=uu⊗
.end

Which completes the proof of $ISPARTN-UU-NN.  

	Notice that $ISPARTN-UU-NN implies that the partitions of ⊗uu can 
be expressed in terms of the partitions of ⊗⊗qd uu⊗.  
Namely we take the partitions of ⊗⊗qd uu⊗ into ⊗⊗sub1 nn⊗ parts
and add ⊗⊗<qa uu>⊗ as the first element of each partition.   
To these we ⊗⊗append⊗ the result of taking the partitions of ⊗⊗qd uu⊗ 
into ⊗nn parts and adding ⊗⊗qa uu⊗ to the first element of each partition.  
These two tacking procedures are implemented by the programs 
⊗tack1 and ⊗tack0 defined by ⊗PNLIST and ⊗PNNLIST recursion respectively.
.begin nofill turnon "∂" group
.n←10

$TACK1: ∂(n)⊗⊗tack1[vv,pl] ← qif qn pl qthen qNIL qelse [vv_._qa pl]_._tack1[vv,qd pl]⊗
$TACK0: ∂(n)⊗⊗tack0[x,pnnl] ← qif qn pnnl qthen qNIL qelse [[x_._qaa pnnl]_._qda pnnl]_._tack0[x,qd pnnl]⊗
.apart 
.group

they are represented by the functions ⊗tack0 and ⊗tack1 satisfying

$TACK0-DEF: ∂(n+4)⊗⊗∀vv pl:tack1[vv,pl] = qif qn pl qthen qNIL qelse [vv_._qa pl]_._tack1[vv,qd pl]⊗
	    ∂(n+4)⊗⊗tack0: PNNLIST → PNNLIST⊗

$TACK1-DEF: ∂(n+4)⊗⊗∀x pnnl:tack0[x,pnnl] = qif qn pnnl qthen qNIL ⊗
            ∂(n+24)⊗⊗ qelse [[x_._qaa pnnl]_._qda pnnl]_._tack1[x,qd pnnl]⊗
	    ∂(n+4)⊗⊗tack1: PNLIST → PNNLIST⊗
.apart 
.group

and we have the immediate corollaries:

$TACK1-NIL: ∂(n+4)⊗⊗∀vv:tack1[vv,qNIL] = qNIL⊗
$TACK1-PNNLL: ∂(n+4)⊗⊗∀vv pll: tack1[vv,pll] = [vv_._qa pll]_._tack1[vv,qd pll]⊗

$TACK0-NIL: ∂(n+4)⊗⊗∀x:tack0[x,qNIL] = qNIL⊗
$TACK0-PNNLL: ∂(n+4)⊗⊗∀x pnnll: tack0[x,pnnll]=[[x_._qaa pnnll]_._qda pnnll]_._tack1[x,qd pnnll]⊗
.end

	The following facts about ⊗tack1 and ⊗tack0 correspond to the clauses of
$ISPARTN-UU-NN.  
.begin nofill turnon "∂"
.n←15

$MEM-TACK1: ∂(n)⊗⊗∀vv pl W:[member[W,tack1[vv,pl]] ≡ ⊗
	    ∂(n+8)⊗⊗∃uull:[W=uull∧qa uull=vv∧member[qd uull,pl]] ]⊗
$MEM-TACK0: ∂(n)⊗⊗∀x pnnl W:[member[W,tack0[x,pnnl]] ≡ ⊗
		∂(n+8)⊗⊗∃uull:[W=uull∧qaa uull=x∧member[qda uull_._qd uull,pnnl]] ]⊗
.end

The proofs of $MEM-TACK1 and $MEM-TACK0 are similar.  We will prove only
$MEM-TACK1.  It is proved by using the $PNLISTINDUCTION schema.  In the
case ⊗⊗pl=qNIL⊗ we must show

⊗⊗⊗∀vv W:[member[W,tack1[vv,qNIL]]≡∃uull:[W=uull∧qa uull=vv∧member[qd uull,qNIL]] ].⊗

⊗⊗tack1[vv,qNIL]=qNIL⊗ by $TACK1-NIL and ⊗⊗¬member[W,qNIL]⊗ by $MEMBER-NIL 
so both sides of the equivalence are false.

In the case ⊗⊗pl≠qNIL⊗ we let ⊗⊗pl=pll⊗ and we have
.begin nofill turnon "∂"
.m←54

⊗⊗member[W,tack1[vv,pll]] ⊗
__⊗⊗≡ W=[vv_._qa pll] ∨ member[W,tack1[vv,qd pll]]⊗ ∂(m-2) $MEMBER-UU,TACK1-PNLL,SEXP 
__⊗⊗≡ W=[vv_._qa pll] ∨ ∃uull:[W=uull∧qa uull=vv∧member[qd uull,qd pll] ].⊗∂(m+5) induction
__⊗⊗≡ ∃uull:[W=uull∧qa uull=vv∧qd uull=qa pll] ∨⊗
__⊗⊗__∃uull:[W=uull∧qa uull=vv∧member[qd uull,qd pll] ⊗∂(m)⊗⊗[vv_._qa pll] ε NEUULIST⊗
__⊗⊗≡ ∃uull:[W=uull∧qa uull=vv∧member[qd uull,pll]] ]⊗ ∂(m)logic of ∃ and $MEMBER-UU 
.end

Which completes the proof.

The program ⊗partn is given by the definition
.begin nofill turnon "∂" group
.n←18

$PARTN: ∂(n)⊗⊗partn[u,n] ← ⊗
∂(n+4)⊗⊗qif qn u qthen [qif n qequal 0 qthen <qNIL> qelse qNIL]⊗
∂(n+4)⊗⊗qelse [qif n equal 0 qthen qNIL qelse ⊗
∂(n+8)⊗⊗tack1[<qa u>,partn[qd u,sub1 n]] * tack0[qa u,partn[qd u,n]] ⊗
.apart
.group

which is represented by the function ⊗partn satisfying 

$PARTN-DEF: ∂(n)⊗⊗∀u n:partn[u,n] =⊗
∂(n+4)⊗⊗qif qn u qthen [qif n qequal 0 qthen <qNIL> qelse qNIL]⊗
∂(n+4)⊗⊗qelse [qif n equal 0 qthen qNIL qelse ⊗
∂(n+8)⊗⊗tack1[<qa u>,partn[qd u,sub1 n]] * tack0[qa u,partn[qd u,n]] ⊗
.apart
.group

with the immediate corollaries

$PARTN-NIL-ZERO: ∂(n)⊗⊗partn[qNIL,0] = <qNIL>⊗
$PARTN-NIL-NN:   ∂(n)⊗⊗∀nn: partn[qNIL,nn] = qNIL⊗
$PARTN-UU-ZERO: ∂(n)⊗⊗∀uu: partn[uu,0] = qNIL⊗
$PARTN-UU-NN: ∂(n)⊗⊗∀uu nn: partn[uu,nn] = ⊗
∂(n+8)⊗⊗tack1[<qa uu>,partn[qd uu,sub1 nn]] * tack0[qa uu,partn[qd uu,nn]] ⊗

.end

The correctness of ⊗partn is stated by

$ISPARTN-COR: ⊗⊗∀u n:∃pl:[partn[u,n]=pl ∧ ∀W:[member[W,pl]≡Ispartn[W,u,n]]].⊗

We prove $ISPARTN-COR by list induction.

In the case ⊗⊗u=qNIL⊗ there are two cases.  If ⊗⊗n=0⊗ then ⊗⊗partn[u,n]=<qNIL>⊗.
Since ⊗⊗<qNIL>⊗ is of sort ⊗PNLIST we need only show

⊗⊗⊗∀W:[member[W,<qNIL>]≡Ispartn[W,qNIL,0]]].⊗

which follow from $MEMBER-NIL, $MEMBER-UU, and $ISPARTN-NIL-ZERO.  
If ⊗⊗n≠0⊗ then ⊗⊗partn[u,n]=qNIL⊗ which is also of sort ⊗PNLIST, so we
need only show

⊗⊗⊗∀W:[member[W,qNIL]≡Ispartn[W,qNIL,n]]]⊗

which follows from $MEMEBER-NIL, and $ISPARTN-NIL-NN.  This takes care of 
the case ⊗⊗u=qNIL⊗.  

In the case ⊗⊗u≠qNIL⊗ we let ⊗⊗uu=u⊗.  If ⊗⊗n=0⊗ then ⊗⊗partn[uu,n]=qNIL⊗ 
and as qNIL is of sort ⊗PNLIST we need only show

⊗⊗⊗∀W:[member[W,qNIL]≡Ispartn[W,uu,0]]]⊗

which follows from $MEMBER-NIL and $ISPARTN-UU-ZERO.  

If ⊗⊗n≠qNIL⊗ we let ⊗⊗n=nn⊗ and assume the induction hypothesis

⊗⊗⊗∀n:∃pl:[partn[qd uu,n]=pl ∧ ∀W:[member[W,pl]≡Ispartn[W,qd uu,n]]].⊗

Now,

⊗⊗⊗partn[uu,nn]=tack1[<qa uu>,partn[qd uu,sub1 nn]] * tack0[qa uu,partn[qd u,nn]] ⊗

and using the induction hypothesis we have for some ⊗pl and ⊗ql 
.begin nofill

⊗⊗⊗partn[qd uu,sub1 nn]=pl ∧ ∀W:[member[W,pl]≡Ispartn[W,qd uu,sub1 nn]]⊗
and
⊗⊗⊗partn[qd uu,nn]=ql ∧ ∀W:[member[W,ql]≡Ispartn[W,qd uu,nn]]].⊗
.end

By $ISPARTN-DEF-NN we have that every member of ⊗ql is of sort ⊗NEUULIST, 
so we may take ⊗ql=qnnl to be of sort ⊗PNNLIST.  Thus 

⊗⊗⊗partn[uu,nn]=tack1[<qa uu>,pl] * tack0[qa uu,qnnl] ⊗  

which is of sort ⊗PNLIST using function mappings for ⊗tack1, ⊗tack0 and ⊗append.  
So we need only show

⊗⊗⊗∀W:[member[W,partn[uu,nn]]≡Ispartn[W,uu,nn]]]⊗

to complete the proof.  This follows by the following argument:

.begin nofill turnon "∂" group
.n←2 m←56

⊗⊗member[W,partn[uu,nn]]⊗
∂(n)⊗⊗≡member[W,tack1[<qa uu>,pl]] ∨ member[W,tack0[qa uu,qnnl]]⊗∂(m);by $MEMBER-UV 
∂(n)⊗⊗≡[∃uull:[W=uull∧qa uull=<qa uu>∧member[qd uull,pl]] ∨⊗
∂(n)⊗⊗__∃uull:[W=uull∧qaa uull=qa uu∧member[qda uull_._qd uull,qnnl]] ]⊗∂(m);by $MEM-TACK1,MEM-TACK0 
∂(n)⊗⊗≡[∃uull:[W=uull∧qa uull=<qa uu>∧Ispartn[qd uull,qd uu,sub1 nn]] ∨⊗
∂(n)⊗⊗__∃uull:[W=uull∧qaa uull=qa uu∧Ispartn[qda uull_._qd uull,qd uu,nn]] ]⊗∂(m) ;by induction hypothesis 
∂(n+2)⊗⊗≡Ispartn[W,uu,nn]]⊗ ∂(m) ;by $ISPARTN-UU-NN 

.end

This completes the proof.  Note that we did not prove ⊗partn to be total
as a separate step.  This is because the clause ⊗⊗∃pl.partn[u,n]=pl⊗
says among other things that ⊗⊗PNLIST partn[u,n]⊗.


.cb |Formal description of domains ⊗⊗UULIST,PNLIST,PNNLIST⊗|

Thus we have the subdomain relations:

.begin nofill turnon "∂" turnoff "{}"
.n←20
.group

∂(n)⊗⊗UULIST = NULL ∪ NEUULIST⊗
∂(n)⊗⊗NULL ∩ NEUULIST = qEMPTY⊗
∂(n)⊗⊗UULIST ⊂ LIST⊗
∂(n)⊗⊗NEUULIST ⊂ NELIST⊗
.apart
.group

∂(n)⊗⊗PNLIST = NULL ∪ NEPNLIST⊗
∂(n)⊗⊗NULL ∩ NEPNLIST = qEMPTY⊗
∂(n)⊗⊗PNLIST ⊂ LIST⊗
∂(n)⊗⊗NEPNLIST ⊂ NELIST⊗
.apart
.group

∂(n)⊗⊗PNNLIST = NULL ∪ NEPNNLIST⊗
∂(n)⊗⊗NULL ∩ NEPNNLIST = qEMPTY⊗
∂(n)⊗⊗PNNLIST ⊂ UULIST⊗
∂(n)⊗⊗NEPNNLIST ⊂ NEUULIST⊗
.end

We will have additional variables ranging over the new sorts.
.begin nofill turnon "∂"
.n←20
.group

∂(n)⊗⊗uul, vvl, wwl ε UULIST⊗
∂(n)⊗⊗uull, vvll, wwll ε NEUULIST⊗
∂(n)⊗⊗pl, ql, rl ε PNLIST⊗
∂(n)⊗⊗pll, qll, rll ε NEPNLIST⊗
∂(n)⊗⊗pnnl, qnnl, rnnl ε PNNLIST⊗
∂(n)⊗⊗pnnll, qnnll, rnnll ε NEPNNLIST⊗
.end

The function mappings for ⊗car, ⊗cdr, and ⊗cons on the new sorts is as follows:

.begin nofill turnon "∂"
.n←20
.group

∂(n)⊗⊗qqa: NEUULIST → NELIST⊗
∂(n)⊗⊗qqd: NELIST → LIST⊗
∂(n)⊗⊗qcons: NELIST qcross UULIST → NEUULIST⊗
.apart
.group

∂(n)⊗⊗qqa: NEPNLIST → UULIST⊗
∂(n)⊗⊗qqd: NEPNLIST → PNLIST⊗
∂(n)⊗⊗qcons: UULIST qcross PNLIST → NEPNLIST⊗
.apart
.group

∂(n)⊗⊗qqa: NEPNNLIST → NEUULIST⊗
∂(n)⊗⊗qqd: NEPNNLIST → PNNLIST⊗
∂(n)⊗⊗qcons: NEUULIST qcross PNNLIST → NEPNNLIST⊗
.end

Since ⊗⊗UULIST⊗s ⊗⊗PNLISTS⊗s and ⊗⊗PNNLIST⊗s are analogous to ⊗⊗LIST⊗s
Thus we have recursion and induction on these domains.  
In particular we have the induction schemata:

.begin nofill
.indent 5,5
.group

$UULISTIND: __⊗⊗qP qNIL∧∀uull:[qP qd uull ⊃ qP uull] ⊃ ∀uul:qP uul⊗
$PNLISTIND: __ ⊗⊗qP qNIL ∧ ∀pll:[qP qd pll ⊃ qP pll] ⊃ ∀pl:qP pl ⊗
$PNNLISTIND: __⊗⊗qP qNIL ∧ ∀pnnll:[qP qd pnnll ⊃ qP pnnll] ⊃ ∀pnnl:qP pnnl .⊗
.end
 
.ss(provexex, Exercises )
.item←0

	This collection of exercises treats properties of association
lists, substitutions, and pattern matching.  These topics are strongly
interrelated and the ability to treat properties of
such programs is fundamental to the general area of symbolic computation.



#. Association lists

	Prove the following facts about association lists.
.begin nofill

	##.	⊗⊗∀u v: [alist u ∧ alist v ⊃ alist[u * v]⊗

	##. 	⊗⊗∀z u v: alist u ∧ alist v ⊃ ⊗
                          ⊗⊗[assoc[z,u*v] = qif qn assoc[z,u] qthen assoc[z,v] qelse assoc[z,u]]⊗

where

     	⊗⊗alist u ← qn u ∨ [¬qat qa u ∧ alist qd u]]]⊗ 

	⊗⊗assoc[x, s] ← qif qn s qthen qNIL qelse qif x = qaa s qthen qa s qelse assoc[x, qd s]⊗
.end

#. Properties of substitutions and substitution lists.

	With function definitions as given below,
⊗⊗subst[x,_y,_z]⊗ is the result of replacing the variable ⊗y by the
S-expression ⊗x wherever ⊗y occurs in ⊗z.  If ⊗s is a list of substitutions of 
the form ⊗⊗y_._x⊗ then ⊗⊗sublis[z,_s]⊗ is the result of "simultaneously" performing
all of the substitutions on the list to ⊗z. If ⊗s1 and ⊗s2 are lists of substitutions
then ⊗s1 @ ⊗s2 is the "composition"  of the two.  Prove the following properties.

.NOFILL

	##.	⊗⊗∀x y z: subst[x, y, z] = sublis[z, <y . x>]⊗

	##.	⊗⊗∀z s1 s2: sublis[z, s1 @ s2] = sublis[sublis[z, s1], s2]⊗

	##. 	⊗⊗∀z s1 s2 s3: sublis[z, s1 @ [s2 @ s3]] = sublis[z, [s1 @ s2] @ s3]⊗

.<<	##.	⊗⊗∀x y z: (¬occur[y, z] ⊃ subst[x, y, z] = z)⊗ 
.>>
	##.	⊗⊗∀x x1 y y1 z: ((y ≠  y1 ∧ ¬occur[y, x1]) ⊃ ⊗
	    		⊗⊗subst[x1, y1, subst[x, y, z]] = subst[subst[x1, y1, x], y, subst[x1, y1, z]])⊗


where

	⊗⊗subst[x, y, z] ← qif qat z qthen [qif y = z qthen x qelse z] ⊗
			⊗⊗qelse subst[x, y, qa z] . subst[x, y, qd z]⊗

.<<	⊗⊗occur[x, y] ← [x = y] ∨ [¬qat y ∧ [occur[x, qa y] ∨ occur[x, qd y]]]⊗. 
.>>
	⊗⊗sublis[x, s] ← qif qat x qthen α{assoc[x, s]α}[λz: qif qn z qthen x qelse qd z]⊗
			⊗⊗qelse sublis[qa x, s] . sublis[qd x, s]⊗

	⊗⊗s1 @ s2 ← subsub[s1, s2] * s2⊗

	⊗⊗subsub[s1, s2] ← qif qn s1 qthen qNIL qelse [qaa s1 . sublis[qda s1, s2]] . subsub[qd s1, s2]⊗
.FILL

#.  Pattern matching 


	The function ⊗inst is one sort of "pattern matcher".  We say that an
S-expression ⊗x is an instance of another S-expression ⊗y if ⊗y can be transformed
into ⊗x by replacing some of the atoms of ⊗y which satisfy ⊗isvar by suitable
values.  (All occurrences of the same variable should be replaced by the
same value.)  ⊗⊗inst[x,_y,_qNIL]⊗ is
$NO if ⊗x is not and instance of the pattern ⊗y, and otherwise is the list of
substitions which will convert ⊗y into ⊗x.  In the latter case we have
⊗⊗x_=_sublis[y,_inst[x,_y,_qNIL]⊗.  Write a definition for ⊗inst and prove that

⊗⊗⊗∀x y u: (inst[x, y, u] ≠ $NO ⊃ x = sublis[y, inst[x, y, u]])⊗

.if false then begin "inst"

	⊗⊗inst[x, y, s] ← qif s = $NO qthen $NO ⊗
		⊗⊗qelse qif qat y qthen [qif isvar y qthen ⊗
				⊗⊗α{assoc[y, s]α}[λz: qif qn z qthen [y . x] . s qelse qif qd z = x qthen s qelse $NO ]⊗
			⊗⊗qelse qif y = x qthen s qelse $NO ]⊗
	    	⊗⊗qelse qif qat x qthen $NO ⊗
		⊗⊗qelse inst[qd x, qd y, inst[qa x, qa y, s]]⊗
.end "inst"

#. Unification

	(This is a fairly substantial exercise.)  

	⊗unify[x,y] attempts to find the most general 
pattern which is an instance of both ⊗x and ⊗y. If no such pattern exists the it
returns $NO, otherwise it returns a list of substitutions which will convert both
⊗x and ⊗y into that pattern.  Write a definition of ⊗unify and prove

	##.	⊗⊗∀x y: (unify[x, y] ≠ $NO ⊃ sublis[x, unify[x, y]] = sublis[y, unify[x, y]])⊗

        ##. 	⊗⊗∀x y: (unify[x, y] = $NO ⊃ ∀s: sublis[x, s] ≠ sublis[y, s])⊗

	##.	⊗⊗∀x y s: (sublis[x, s] = sublis[y, s] ⊃ ∃s1: ∀z: sublis[z, s] = sublis[z, unify[x, y] @ s1])⊗



. if false then begin "unify"

 	⊗⊗isvar x ← x = $U ∨ x = $V ∨ x = $W ∨ x = $X ∨ x = $Y ∨ x = $Z ⊗

	⊗⊗unify[x, y] ← qif x = y qthen qNIL⊗
		⊗⊗qelse qif isvar x qthen [qif occur[x, y] qthen $NO qelse <x . y>]⊗
		⊗⊗qelse qif isvar y qthen [qif occur[y, x] qthen $NO qelse <y . x>]⊗
		⊗⊗qelse qif [qat x ∨ qat y] qthen $NO ⊗
		⊗⊗qelse α{unify[qa x,qa y]α}⊗
			⊗⊗[λs1: qif s1 = $NO qthen $NO ⊗
			    ⊗⊗qelse α{unify[sublis[qd x, s1],sublis[qd y, s1]]α}⊗
				⊗⊗[λs2: qif s2 = $NO qthen $NO qelse s1 @ s2]]⊗

.end "unify"